1. Field of the Invention
The present invention relates to a logic circuit verification device to verify the logic circuit equivalence and a method for such verification, and particularly relates to a logic circuit verification device to verify the equivalence with partitioning the logic circuits to be verified into subcircuits and a method therefor.
2. Description of the Related Art
In conventional circuit designing, the equivalence of two circuits has been verified by partitioning the two circuits to be verified into subcircuits and verifying the equivalence for each subcircuit. Circuits have been partitioned with focusing the registers first, and then with making use of intermediate signal name information. The compared subcircuits are associated according to the register signal name information and intermediate signal name information so that the equivalence is verified for each corresponding set of subcircuits.
For a conventional equivalence checking device used for circuit equivalence verification of this type and a method therefor, the user has to specify the register signal name information and intermediate signal name information to be used in the circuit partitioning as described above. This type of conventional technologies include, for example, a system disclosed in the literature "Logic Verification System: CONDOR" (Mukoyama et al., Design Automation Research Association 63-3, pp. 17-22, Information Processing Society of Japan). FIG. 10 shows the system configuration according to the conventional technology as described in the literature above.
As shown in FIG. 10, a conventional system described in the above literature inputs the circuit description of the circuits to be verified at a combinational circuit making section 1002 and creates subcircuits by partitioning the circuits to be verified according to the register signal name information obtained from the specification description. At a logic verification section 1001, it further partitions, when necessary, the subcircuits prepared by the combinational circuit making section 1002 according to the intermediate signal name information obtained from the specification description and collates the subcircuits one by one.
Other similar conventional technologies include the invention disclosed in Japanese Patent Application Laid-open (Kokai) No. Heisei 6-162129 "Logic circuit Verification Device". This invention discloses the device which partitions the verified circuits to make the subcircuits where the signal as which the signal name is the same is the output signal between two verified circuits and the primary input or the signal to which the verification result is corresponding is an input signal when partitioning the verified circuits.
Another example of conventional technologies is the one disclosed in the literature "A Novel Framework for Logic Verification in a Synthesis Environment" (Wolfgang Kunz, Member, IEEE, Dhiraj K. Pradhan, Fellow, IEEE, and Subodh M. Reddy, IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 15, NO. 1, JANUARY 1996). This literature describes the technology which, on the assumption that the verified circuits are combinational ones, partitions the verified circuits into subcircuits and collates the subcircuits.
According to the conventional technology described in the literature "Logic Verification System: CONDOR" above, however, collation is made for each subcircuit prepared by partitioning the circuits at the combinational circuit making section and the logic collation section without any rule to choose the subcircuits to be compared, or a rule for correspondence of subcircuits to be compared. Besides, conventional technologies do not account for the configuration of the verified circuits and correspondence of the compared subcircuits should be specified manually, which results in a drawback of much labor.
In addition, the partitioning position of the verified circuit is decided by the agreement of the signal name according to the conventional technology as described in the above literature. Therefore, when the signal name of a suitable correspondence point for partitioning is different, the circuits cannot be divided with the correspondence concerned point. The conventional technology has the fault by which an appropriate partial circuit cannot be made in the above case.
Further, the conventional technology described in the literature "A Novel Framework for Logic Verification in a Synthesis Environment" assumes that the verified circuits are combinational ones, and cannot be applied to verification of sequential circuits.